\begin{tabbing}
es{-}secret{-}server\=\{\$table:ut2, \$encrypt:ut2, \$decrypt:ut2\}\+
\\[0ex](${\it es}$; $T$; $L$; $i$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=let ${\it ds}$ = "\$table" : secret{-}table($T$) in \+
\\[0ex]l\_all($L$;IdLnk;$l$.destination($l$) $=$ $i$ $\in$ Id
\\[0ex]\& es{-}kind{-}sends{-}iff(${\it es}$;rcv($l$,"\$encrypt");\=($\mathbb{N}$+Atom1)\+
\\[0ex]$\times$data($T$);lnk{-}inv($l$);"\$encrypt";\=$\mathbb{N}$\+
\\[0ex]$\times$Atom1;${\it ds}$;$e$.next(es{-}when
\-\-\\[0ex](${\it es}$; "\$table"; $e$)))
\\[0ex]\& \=es{-}kind{-}sends{-}iff(${\it es}$;rcv($l$,"\$decrypt");\=($\mathbb{N}$+Atom1)\+\+
\\[0ex]$\times$Atom1;lnk{-}inv($l$);"\$decrypt";data($T$);${\it ds}$;$e$.decrypt(es{-}when
\-\\[0ex](${\it es}$; "\$table"; $e$);es{-}val(${\it es}$; $e$))))
\-\\[0ex]\& \=frame{-}p(${\it es}$; $i$; secret{-}table($T$); "\$table"; map($\lambda$$l$.rcv($l$,"\$encrypt");$L$))\+
\\[0ex]\& \=l\_all($L$;IdLnk;$l$.effect{-}p(${\it es}$;$i$;${\it ds}$;rcv($l$,"\$encrypt");\=($\mathbb{N}$+Atom1)\+\+
\\[0ex]$\times$data($T$);"\$table";$\lambda$$s$,$v$.
\-\\[0ex]encrypt($s$."\$table";$v$)))
\\[0ex]\& alle{-}at(${\it es}$;$i$;$e$.$\exists$${\it e'}$:es{-}E(${\it es}$).
\\[0ex]es{-}leaks(${\it es}$;$e$;"\$table";${\it e'}$)
\\[0ex]$\Rightarrow$ \=l\_exists($L$;IdLnk;$l$.es{-}kind(${\it es}$; $e$) $=$ rcv($l$,"\$encrypt") $\in$ Knd\+
\\[0ex]\& es{-}kind(${\it es}$; ${\it e'}$) $=$ rcv(lnk{-}inv($l$),"\$encrypt") $\in$ Knd
\\[0ex]$\vee$ \=es{-}kind(${\it es}$; $e$) $=$ rcv($l$,"\$decrypt") $\in$ Knd\+
\\[0ex]\& es{-}kind(${\it es}$; ${\it e'}$) $=$ rcv(lnk{-}inv($l$),"\$decrypt") $\in$ Knd))
\-\-\\[0ex]\& alle{-}at(${\it es}$;$i$;$e$.$\neg$es{-}copies(${\it es}$;$e$;"\$table"))
\\[0ex]\& alle{-}at(${\it es}$;$i$;$e$.\=es{-}first(${\it es}$; $e$)\+
\\[0ex]$\Rightarrow$ \=atoms{-}distinct(es{-}when(${\it es}$; "\$table"; $e$))\+
\\[0ex]\& ptr(es{-}when(${\it es}$; "\$table"; $e$)) $=$ 0 $\in$ $\mathbb{N}$
\\[0ex]\& (\=$\forall$$n$:$\mathbb{N}$, $j$:Id.\+
\\[0ex]$n$$<\parallel$es{-}when(${\it es}$; "\$table"; $e$)$\parallel$ 
\\[0ex]$\Rightarrow$ es{-}atom(${\it es}$;$j$;st{-}atom(es{-}when(${\it es}$; "\$table"; $e$);$n$))
\\[0ex]$\Rightarrow$ $j$ $=$ $i$ $\in$ Id))
\-\-\-\-\-\-
\end{tabbing}